COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00007 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source
.bb EXTENSIONAL FORMS

	Consider first ordinary forms, i.e. expressions built
from symbols for constants, variables and functions and possibly
quantifiers and the Church lambda operator.  Such a form will
have certain free variables, and its value will depend on the
values assigned to the free variables.  We call two forms
⊗extensionally ⊗equivalent if they have the same value for all
assignments of values to the free variables they contain.  Thus
if + has its usual interpretation on the integers, the
forms ⊗x+y and ⊗y+x are extensionally equivalent, but neither of
them is extensionally equivalent to ⊗u+v, because assigning ⊗x 
and ⊗y the value 0 and ⊗u and ⊗v the value 1 gives the forms
different values.

	Extensional forms can be regarded as the equivalence classes of this
equivalence relation, but instead of first introducing ordinary forms
and the equivalence relation, we will define extensional forms inductively
from the symbols for constants, variables, and functions.  In order to
motivate the reader's attention to a somewhat boring inductive
definition, we remark on the following virtues of extensional forms:
First they have no bound variables which simplifies the statement of
the laws of substitution, and second all the ways of building up
extensional forms are by the application of functions to constituent
forms; even ⊗λ(x,e) is just a function of two extensional forms ⊗x 
and ⊗e.  Consequently the syntax and semantics of extensional forms
can be axiomatized in first order logic.  This is important for the
applications to mathematical theory of computation and to the theory
of concepts.

	We start with a simplified theory:

	Let ⊗D be a domain, e.g. the integers or people or concepts
of integers or concepts of people.  Let ⊗V be an infinite class of
objects called variables, and let ⊗E be another class of objects
called environments.  Let %2value: V %8x%2 E → D%1 be a distinguished
function.  We will call %2value(x,e)%1 the value of the variable ⊗x
in the environment ⊗e. We assume an axiom of extensionality for
environments, namely

Ext!!ext1:	%2∀e1 e2.(∀x.(value(x,e1) = value(x,e2)) ⊃ e1 = e2)%1.

Ext{eq ext1} implies that environments can be identified with certain
functions from variables to domain elements.  However, we cannot conclude
that all such functions are represented by environments.

	Next we have the assignment function %2assign: V %8x%2 D %8x%2 E → E%1.
It satisfies the axioms

Ext!!ext2:	%2∀x d e.(value(x,assign(x,d,e)) = d)%1

and

Ext!!ext3:	%2∀x y d e.(y≠x ⊃ value(y,assign(x,d,e)) = value(y,e))%1.